Nuprl Lemma : fun-path-induction 11,40

T:Type, f:(TT), R:(TT(T List)).
(x:TR(x,x,[x]))
 (L:(T List), xyz:T. (x = f(y))  ((x = y))  R(y,z,[y / L])  R(x,z,[xy / L]))
 {L:(T List), xy:Tx=f*(y) via L  R(x,y,L)} 
latex


Definitionst  T, type List, A List, s = t, x:AB(x), x:AB(x), [car / cdr], y=f*(x) via L, Type, f(a), x(s1,s2,s3), A, , a < b, x:A  B(x), P & Q, #$n, , hd(l), ||as||, Void, P  Q, False, A  B, i  j , [], left + right, P  Q, Dec(P), b, x:AB(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xLP(x), (xL.P(x)), {T}, P  Q, <ab>,
Lemmasnon neg length, fun-path-cons, decidable lt, not wf, hd wf, length wf1, fun-path wf

origin